package subtyped
import scala.util.parsing.combinator.Parsers


object SubTypedLambda{
  
  def eval(line: String) {
    val canontree=parse(line)
    typeCheck(canontree)
    eval(canontree)
  }
  
  def parse(line: String) = {
    val rawtree = TypedLambdaParser.parseString(line) getOrElse exit(-1)
    val (_,canontree) = NameContext.desugar(rawtree)
    Console.println("code= " +canontree.toString_(new Context[NameBinding](Nil)))
    Console.println(" AST= " + canontree.toString)
    canontree
  }
  
  def typeCheck(canontree: LTerm) = println("   :: "+LTerm.typeOf(canontree))
  def eval(canontree: LTerm) =  println(" ===> " + (LTerm.eval(canontree)) .toString_(new Context[NameBinding](Nil)))
 
}
 


     
import scala.util.parsing.input.StreamReader
import java.io.StringReader

object TypedLambdaParser extends TypedLambdaParser
  {
    def parseString(str: String) : Option[LTerm]= {
      val in = StreamReader(new StringReader(str))
      parse(in) match
      {
      case Success(term, _) =>
      {
        Some(term)
      }
      case Failure(msg, remainder) => println("Failure: "+msg+"\n"+"Remainder: \n"+remainder.pos.longString) ;None
      case Error(msg, remainder)   => println("Error: "+msg+"\n"+"Remainder: \n"+remainder.pos.longString) ; None
    }
    }

  }




object NameContext{

  def desugar(t: LTerm):(Context[NameBinding],LTerm)= desugar(new Context[NameBinding](Nil) , t)
  def desugar(ctx:Context[NameBinding] , t: LTerm):(Context[NameBinding],LTerm) = t match {
    
    case Lam(n,ty,t) => n match { case Name(str) => {
      val ctx2 = NameContext.addName(ctx, str) // TODO: ctx2 = ctx + str
      val (_, t2) = desugar(ctx2, t) // Q: interpret: discarding resulting ctx
      (ctx, L(str,ty,t2)) //
    }}
    case Ref(Name(str)) =>  {
      val i = getDeBruijnIndex(ctx,str)
      (ctx, V(i))
    }
    case Let(Name(str),t1,t2) =>
      val ctx2 = NameContext.addName( ctx, str)
      val (_,t1_) = desugar(ctx, t1)
      val (_,t2_) = desugar(ctx2, t2)
      (ctx, Let(Name(str),t1_,t2_))
    case App(t1,t2)         => 
      val (_, t1_) = desugar(ctx, t1)
      val (_, t2_) = desugar(ctx, t2)
      (ctx,A(t1_,t2_))
      
    case RecProj(t1,i)      => 
      val (_,t1_) = desugar(ctx, t1)
      (ctx, RecProj(t1_,i))
    case Record(list)       => {
      def f( s:String,t:LTerm) : (String,LTerm) = 
        (s, desugar(ctx,t)._2)
      val list_ = list.map( Function.tupled(f))
      (ctx, Record(list_))
    }
    
    case Unit()             => (ctx,Unit)
    case Lit(n)             => (ctx,Lit(n))
    case Name(n)            => throw new Exception()
    
    case Tru() => (ctx,Tru)
    case Fls() => (ctx,Fls)
    case If(c,p,n) => {
      val (_,c2) = desugar(ctx,c)
      val (_,p2) = desugar(ctx,p)
      val (_,n2) = desugar(ctx,n)
      (ctx,If(c2,p2,n2))
    }
    case V(n)               => (ctx,V(n))
    case L(x,ty,t)          => (ctx, L(x,ty,t))
    case A(t1, t2)          => (ctx,A(t1,t2))
    
    case TyBool()           => (ctx, TyBool)
    case TyInt()            => (ctx, TyInt)
    case TyArr(ty1,ty2)     => (ctx, (TyArr(ty1,ty2)))
    /*
    case PrimPlus()         => (ctx,PrimPlus)
    case PrimMinus()        => (ctx,PrimMinus)
    case PrimMultiply()     => (ctx,PrimMultiply)
    case PrimDivide()       => (ctx,PrimDivide)
    case PrimEquals()       => (ctx,PrimEquals)
    */
  }
  def addName(ctx: Context[NameBinding], n: String) = {
    ctx + (n,NameBinding(n))
  }

  def getDeBruijnIndex(ctx: Context[NameBinding], n: String)= ctx.getIndexOfName(n)
  def pickDisplayName(n: String, ctx: Context[NameBinding])
              :(Context[NameBinding],String)= {
    if (ctx.isNameBound(n)) pickDisplayName(n+"'",ctx)
    else (ctx + (n, NameBinding(n)), n)

  }
    

}









